perm filename MASON.1[LET,JMC] blob sn#864712 filedate 1988-08-05 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input jmclet
C00006 ENDMK
CāŠ—;
\input jmclet
\jmclet
\address
Mr. Lee Madden
Assistant Director Foreign Student Services
Bechtel International Center
Stanford University
\bigskip
Subject:  Intent to hire Ian Mason
\body

Dear Mr. Madden:

It is my intent to hire Dr. Ian Alistar Mason as a research associate
in the Stanford Computer Science Department for a minimum of  three years,
at a starting salary of $\$44,000$ per year.

Job description: \quad
The position to be filled by Mason is for basic research in formal
reasoning with focus on programming language theory.  The candidate should
have a strong background in mathematical logic including knowledge of
model theory, recursion theory, and proof theory; experience in
formalizing programming language semantics and ability to apply logic to
the study mathematical properties of language constructs and to develop
tools for reasoning about programs and systematic transformation of
programs; and interest in studying semantics of expressive languages which
include function abstractions, non-local control mechanisms, sharing and
updating mechanisms.  Work will involve collaboration with ongoing
projects in the formal reasoning group which include both informal and
formal reasoning about programs and about the objects programs act on.

Qualifications of the candidate:\quad
Dr. Mason is extremely well qualified for this position.  As an
undergraduate in Australia and as a graduate student at Stanford Mason did
research in logic including model theory and proof theory.  His PhD
research treated semantics of Lisp including memory operations.  This is a
very difficult problem.  Mason's thesis included a precise mathematical
semantics, many non-trivial properties of the model theory including a
variety of decidability results and an axiomatization of program equivalence
that permits proof of a rich class of properties of programs and a basis
for a theory of transformations of such programs.  Since receiving his
PhD Mason
has been associated with the Edinburgh Laboratory for Foundations of
Computer Science working on a system for formalizing logics.  In addition
he has continued research on his thesis topic in collaboration with Dr. C.
Talcott of our group.  Mason is very bright and has shown himself capable
of making important contributions to the understanding of semantics of
programming languages and of bringing fresh insights to many of the hard
problems in programming language theory.

\closing
Sincerely,
John McCarthy
Professor
\endletter
\end